(* $Id: verificationGenerationEnv.mli 162 2007-11-08 09:40:57Z yann.regisgianas $ *)

(* Pangolin, a functional programming language for correct programs.
   Copyright (C) 2007, Yann Régis-Gianas, François Pottier.
   Contact: yann.regisgianas@gmail.com

   This program is free software: you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation, either version 3 of the License, or
   any later version.

   This program is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program.  If not, see <http://www.gnu.org/licenses/>. *)

(** FIXME *)
type t 

(** FIXME *)
type proofs = (t * XCoreSyntax.lformula) list

(** FIXME *)
val bind_atom : XCoreSyntax.Var.AtomIdMap.key -> t -> t

(** FIXME *)
val idmap : t -> XCoreSyntax.var XCoreSyntax.Identifier.Map.t

(** FIXME *)
val atomidmap : t -> XCoreSyntax.Var.AtomIdMap.t

(** FIXME *)
val ienv : t -> XCoreInternals.env

(** FIXME *)
val initial_env : t

(** FIXME *)
val unsafe_export_formula :
  XCoreSyntax.Var.AtomIdMap.t ->
  XCoreSyntax.formula -> XCoreSyntax.Raw.formula

(** FIXME *)
val print_formula : t -> XCoreSyntax.formula -> string

(** FIXME *)
val bind_type_scheme :
  Position.t ->
  t -> XCoreSyntax.Var.AtomIdMap.key -> XCoreSyntax.type_scheme -> t

(** FIXME *)
val bind_dataconstructor_type_scheme :
  Position.t ->
  t -> XCoreSyntax.Var.AtomIdMap.key -> XCoreSyntax.type_scheme -> t

(** FIXME *)
val bind :
  Position.t ->
  t -> XCoreSyntax.Var.AtomIdMap.key -> XCoreSyntax.term_type -> t

(** FIXME *)
val lookup : 'a -> t -> XCoreSyntax.Var.Atom.t -> XCoreSyntax.type_scheme

(** FIXME *)
val bind_logic_scheme :
  Position.t ->
  t -> XCoreSyntax.Var.AtomIdMap.key -> XCoreSyntax.formula_type_scheme -> t

(** FIXME *)
val bind_logic :
  Position.t ->
  t -> XCoreSyntax.Var.AtomIdMap.key -> XCoreSyntax.formula_type -> t

(** FIXME *)
val lift_term_type : XCoreSyntax.term_type -> XCoreSyntax.formula_type

(** FIXME *)
val lift_type_scheme :
  XCoreSyntax.type_scheme -> XCoreSyntax.formula_type_scheme

(** FIXME *)
val lookup_logic :
  'a -> t -> XCoreSyntax.Var.Atom.t -> XCoreSyntax.formula_type_scheme

(** FIXME *)
val introduce_rigid_type_variable :
  Position.t -> t -> XCoreSyntax.Var.AtomIdMap.key -> t

(** FIXME *)
val introduce_rigid_type_variables :
  Position.t -> XCoreSyntax.Var.AtomIdMap.key list -> t -> t

(** FIXME *)
val bind_type_constructor :
  'a -> t -> XCoreSyntax.Var.AtomIdMap.key -> XCoreSyntax.kind -> t

(** FIXME *)
val bind_type_definition :
  Position.position ->
  t ->
  XCoreSyntax.tid -> XCoreSyntax.kind -> XCoreSyntax.type_definition -> t

(** FIXME *)
val display_def :
  t ->
  Position.position ->
  XCoreSyntax.var ->
  XCoreSyntax.formula_type_scheme -> XCoreSyntax.predicate_definition -> unit

(** Bind a predicate definition in the environment. *)
val bind_predicate_definition :
  Position.position ->
  t ->
  XCoreSyntax.var ->
  XCoreSyntax.formula_type_scheme -> XCoreSyntax.predicate_definition -> t

(** FIXME *)
val bind_logic_value :
  Position.t -> t -> XCoreSyntax.id -> XCoreSyntax.formula_type -> t

(** FIXME *)
val bind_logic_function :
  Position.t -> t -> XCoreSyntax.id -> XCoreSyntax.formula_type_scheme -> t

(** FIXME *)
val bind_logic_function_definition :
  Position.position ->
  t ->
  XCoreSyntax.id ->
  XCoreSyntax.formula_type_scheme ->
  XCoreSyntax.logic_function_definition -> t

(** FIXME *)
val handle_error : t -> (unit -> 'a) -> 'a

(** FIXME *)
val hypothesis_id :
  Position.t -> UniqueIdentifier.t option -> UniqueIdentifier.t

(** FIXME *)
val assume :
  XCoreSyntax.fact_status -> bool ->
  Position.position ->
  t -> ?name:UniqueIdentifier.t -> XCoreSyntax.lformula -> t

val assume_by_semantic :
  Position.position ->
  t -> ?name:UniqueIdentifier.t -> XCoreSyntax.lformula -> t

(** FIXME *)
val show_one :
  Position.t ->
  bool ->
  t * (t * XCoreSyntax.lformula) list ->
  ?name:'a -> XCoreSyntax.lformula -> (t * XCoreSyntax.lformula) list

(** FIXME *)
val show :
  Position.t ->
  bool ->
  t * (t * XCoreSyntax.lformula) list ->
  ?name:'a -> XCoreSyntax.lformula -> (t * XCoreSyntax.lformula) list

(** FIXME *)
val have :
  bool ->
  Position.position ->
  t * (t * XCoreSyntax.lformula) list ->
  ?name:UniqueIdentifier.t ->
  XCoreSyntax.lformula -> t * (t * XCoreSyntax.lformula) list

(** FIXME *)
val assume_eq :
  Position.position ->
  t ->
  XCoreSyntax.formula_type -> XCoreSyntax.formula -> XCoreSyntax.formula -> t

(** FIXME *)
val have_eq_pattern :
  Position.position ->
  t ->
  XCoreSyntax.formula_type -> XCoreSyntax.formula -> XCoreSyntax.pattern -> t

(** FIXME *)
val have_neq_pattern :
  Position.position ->
  t ->
  XCoreSyntax.formula_type ->
  XCoreSyntax.formula ->
  (XCoreSyntax.var * XCoreSyntax.term_type) list -> XCoreSyntax.pattern -> t

(** FIXME *)
val empty_proofs : 'a list

(** FIXME *)
val is_dataconstructor : XCoreSyntax.Var.Atom.t -> t -> bool

(** FIXME *)
val pcons :
  XCoreSyntax.program -> XCoreSyntax.component -> XCoreSyntax.program

(** FIXME *)
val type_def_of : XCoreSyntax.Var.Atom.t -> t -> XCoreSyntax.type_definition

(** FIXME *)
val proof_as_term : t * XCoreSyntax.lformula -> XCoreSyntax.program

(** FIXME *)
val export_proof : t * XCoreSyntax.lformula -> XCoreSyntax.Raw.program

(** FIXME *)
val options : unit -> Options.t

val is_trace_enabled : unit -> bool

val as_pfol : t -> PFOLEnv.env
